(set-logic ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-fun tptp.p0 () Bool)
(declare-fun tptp.q0 () Bool)
(declare-fun tptp.r0 () Bool)
(declare-fun tptp.s0 () Bool)
(assert (=> (and tptp.p0 (not tptp.q0)) (or tptp.r0 (not tptp.s0))))
(declare-fun tptp.p ($$unsorted) Bool)
(declare-fun tptp.a () $$unsorted)
(declare-fun tptp.q ($$unsorted $$unsorted) Bool)
(declare-fun tptp.f ($$unsorted) $$unsorted)
(declare-fun tptp.g ($$unsorted $$unsorted $$unsorted) $$unsorted)
(declare-fun tptp.r ($$unsorted $$unsorted $$unsorted) Bool)
(declare-fun tptp.b () $$unsorted)
(declare-fun tptp.s ($$unsorted) Bool)
(assert (forall ((X $$unsorted)) (=> (or (tptp.p X) (not (tptp.q X tptp.a))) (exists ((Y $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f Y))) (and (tptp.r X _let_1 (tptp.g X _let_1 Z)) (not (tptp.s (tptp.f (tptp.f (tptp.f tptp.b)))))))))))
(assert (exists ((Y $$unsorted)) (forall ((X $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f Y))) (or (= _let_1 (tptp.g X _let_1 Z)) (not (= (tptp.f (tptp.f (tptp.f tptp.b))) tptp.a)) (= X _let_1))))))
(assert (or true false))
(declare-fun |tptp.'A proposition'| () Bool)
(declare-fun |tptp.'A predicate'| ($$unsorted) Bool)
(declare-fun |tptp.'A constant'| () $$unsorted)
(declare-fun |tptp.'A function'| ($$unsorted) $$unsorted)
(declare-fun |tptp.'A _'quoted __ escape_''| () $$unsorted)
(assert (or |tptp.'A proposition'| (|tptp.'A predicate'| tptp.a) (tptp.p |tptp.'A constant'|) (tptp.p (|tptp.'A function'| tptp.a)) (tptp.p |tptp.'A _'quoted __ escape_''|)))
(assert (forall ((X $$unsorted)) (= (=> (not (tptp.q X tptp.a)) (tptp.p X)) (exists ((Y $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f Y))) (xor (tptp.r X _let_1 (tptp.g X _let_1 Z)) (not (tptp.s (tptp.f (tptp.f (tptp.f tptp.b)))))))))))
(declare-fun $$rtu (Real) $$unsorted)
(declare-fun $$utr ($$unsorted) Real)
(assert (let ((_let_1 (to_real 123))) (= _let_1 ($$utr ($$rtu _let_1)))))
(assert (forall ((X $$unsorted)) (=> (or (tptp.p X) (not (tptp.q X tptp.a))) (exists ((Y $$unsorted) (Z $$unsorted)) (let ((_let_1 (tptp.f Y))) (and (tptp.r X _let_1 (tptp.g X _let_1 Z)) (not (tptp.s (tptp.f (tptp.f (tptp.f tptp.b)))))))))))
(declare-fun tptp.h () $$unsorted)
(assert (tptp.p tptp.h))
(assert (not (exists ((X $$unsorted)) (tptp.p X))))

(declare-fun tptp.ia1 () Bool)
(assert tptp.ia1)
(declare-fun tptp.ia2 () Bool)
(assert tptp.ia2)
(declare-fun tptp.ia3 () Bool)
(assert tptp.ia3)
(set-info :filename SYN000+1)
(check-sat-assuming ( true ))
